import MyTactic.Basic
import LeanProject.ClusterLimit

-- 逐步证明 2 ≤ 6
example : 2 ≤ 6 := by
  apply Nat.le_step -- 2 ≤ 5
  apply Nat.le_step -- 2 ≤ 4
  apply Nat.le_step -- 2 ≤ 3
  apply Nat.le_step -- 2 ≤ 2
  apply Nat.le_refl -- 完成证明

-- ❌ 单独使用 repeat 无法完成证明
example : 2 ≤ 6 := by
  repeat (apply Nat.le_step)
  sorry

-- ✅ 组合使用 repeat 和 first 完成证明
example : 2 ≤ 6 := by
  repeat (first | apply Nat.le_refl | apply Nat.le_step)

-- 2
example : 2 ≤ 6 := by
  repeat 
    first | apply Nat.le_step | apply Nat.le_refl
  
  
  
-----------使用自定义tactic证明-------------------------------
example : 2 ≤ 6 := by
  repeat_apply Nat.le_refl or Nat.le_step

example : 30 < 39 := by
  repeat_apply Nat.le_refl or Nat.le_step

example : 30 < 40 := by
  repeat_apply Nat.succ_le_succ or Nat.zero_le
  
def main : IO Unit := do
  -- 测试用例实现
  IO.println "Running tests..."
  -- 测试代码
  